MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , +(@x, @y) -> #add(@x, @y) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) } Weak Trs: { #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We add following dependency tuples: Strict DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , firstline#1^#(nil()) -> c_10() , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#2^#(nil(), @x, @xs, @y) -> c_30() , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) } Weak DPs: { #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , firstline#1^#(nil()) -> c_10() , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#2^#(nil(), @x, @xs, @y) -> c_30() , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) } Weak DPs: { #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,4,5,6,7,10,18,22,25,27,28,30,34,37} by applications of Pre({1,2,3,4,5,6,7,10,18,22,25,27,28,30,34,37}) = {8,9,16,17,19,20,23,24,26,33,35,36,39}. Here rules are labeled as follows: DPs: { 1: #abs^#(#0()) -> c_1() , 2: #abs^#(#neg(@x)) -> c_2() , 3: #abs^#(#pos(@x)) -> c_3() , 4: #abs^#(#s(@x)) -> c_4() , 5: #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , 6: #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 7: +^#(@x, @y) -> c_7(#add^#(@x, @y)) , 8: firstline^#(@l) -> c_8(firstline#1^#(@l)) , 9: firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , 10: firstline#1^#(nil()) -> c_10() , 11: lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , 12: lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , 13: lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , 14: lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 15: lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , 16: lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , 17: lcs#2^#(nil()) -> c_15(#abs^#(#0())) , 18: lcs#3^#(::(@len, @_@1)) -> c_16() , 19: lcs#3^#(nil()) -> c_17(#abs^#(#0())) , 20: lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , 21: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , 22: lcstable#3^#(nil(), @l2, @x) -> c_22() , 23: newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , 24: newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , 25: newline#1^#(nil(), @lastline, @y) -> c_28() , 26: max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , 27: max#1^#(#false(), @a, @b) -> c_25() , 28: max#1^#(#true(), @a, @b) -> c_26() , 29: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , 30: newline#2^#(nil(), @x, @xs, @y) -> c_30() , 31: newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , 32: newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , 33: right^#(@l) -> c_32(right#1^#(@l)) , 34: right#1^#(::(@x, @xs)) -> c_38() , 35: right#1^#(nil()) -> c_39(#abs^#(#0())) , 36: newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , 37: newline#6^#(@elem, @nl) -> c_37() , 38: newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , 39: newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , 40: #eq^#(#0(), #0()) -> c_40() , 41: #eq^#(#0(), #neg(@y)) -> c_41() , 42: #eq^#(#0(), #pos(@y)) -> c_42() , 43: #eq^#(#0(), #s(@y)) -> c_43() , 44: #eq^#(#neg(@x), #0()) -> c_44() , 45: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 46: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 47: #eq^#(#pos(@x), #0()) -> c_47() , 48: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 49: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 50: #eq^#(#s(@x), #0()) -> c_50() , 51: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 52: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 53: #eq^#(::(@x_1, @x_2), nil()) -> c_53() , 54: #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , 55: #eq^#(nil(), nil()) -> c_55() , 56: #ckgt^#(#EQ()) -> c_68() , 57: #ckgt^#(#GT()) -> c_69() , 58: #ckgt^#(#LT()) -> c_70() , 59: #compare^#(#0(), #0()) -> c_56() , 60: #compare^#(#0(), #neg(@y)) -> c_57() , 61: #compare^#(#0(), #pos(@y)) -> c_58() , 62: #compare^#(#0(), #s(@y)) -> c_59() , 63: #compare^#(#neg(@x), #0()) -> c_60() , 64: #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , 65: #compare^#(#neg(@x), #pos(@y)) -> c_62() , 66: #compare^#(#pos(@x), #0()) -> c_63() , 67: #compare^#(#pos(@x), #neg(@y)) -> c_64() , 68: #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , 69: #compare^#(#s(@x), #0()) -> c_66() , 70: #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , 71: #add^#(#0(), @y) -> c_71() , 72: #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , 73: #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 74: #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , 75: #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 76: #and^#(#false(), #false()) -> c_84() , 77: #and^#(#false(), #true()) -> c_85() , 78: #and^#(#true(), #false()) -> c_86() , 79: #and^#(#true(), #true()) -> c_87() , 80: #pred^#(#0()) -> c_76() , 81: #pred^#(#neg(#s(@x))) -> c_77() , 82: #pred^#(#pos(#s(#0()))) -> c_78() , 83: #pred^#(#pos(#s(#s(@x)))) -> c_79() , 84: #succ^#(#0()) -> c_80() , 85: #succ^#(#neg(#s(#0()))) -> c_81() , 86: #succ^#(#neg(#s(#s(@x)))) -> c_82() , 87: #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) } Weak DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#3^#(::(@len, @_@1)) -> c_16() , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , right#1^#(::(@x, @xs)) -> c_38() , newline#6^#(@elem, @nl) -> c_37() , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {9,10,15,20,23} by applications of Pre({9,10,15,20,23}) = {4,8,19,21,22}. Here rules are labeled as follows: DPs: { 1: firstline^#(@l) -> c_8(firstline#1^#(@l)) , 2: firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , 3: lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , 4: lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , 5: lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , 6: lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 7: lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , 8: lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , 9: lcs#2^#(nil()) -> c_15(#abs^#(#0())) , 10: lcs#3^#(nil()) -> c_17(#abs^#(#0())) , 11: lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , 12: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , 13: newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , 14: newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , 15: max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , 16: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , 17: newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , 18: newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , 19: right^#(@l) -> c_32(right#1^#(@l)) , 20: right#1^#(nil()) -> c_39(#abs^#(#0())) , 21: newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , 22: newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , 23: newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , 24: #abs^#(#0()) -> c_1() , 25: #abs^#(#neg(@x)) -> c_2() , 26: #abs^#(#pos(@x)) -> c_3() , 27: #abs^#(#s(@x)) -> c_4() , 28: #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , 29: #eq^#(#0(), #0()) -> c_40() , 30: #eq^#(#0(), #neg(@y)) -> c_41() , 31: #eq^#(#0(), #pos(@y)) -> c_42() , 32: #eq^#(#0(), #s(@y)) -> c_43() , 33: #eq^#(#neg(@x), #0()) -> c_44() , 34: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 35: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 36: #eq^#(#pos(@x), #0()) -> c_47() , 37: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 38: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 39: #eq^#(#s(@x), #0()) -> c_50() , 40: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 41: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 42: #eq^#(::(@x_1, @x_2), nil()) -> c_53() , 43: #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , 44: #eq^#(nil(), nil()) -> c_55() , 45: #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 46: #ckgt^#(#EQ()) -> c_68() , 47: #ckgt^#(#GT()) -> c_69() , 48: #ckgt^#(#LT()) -> c_70() , 49: #compare^#(#0(), #0()) -> c_56() , 50: #compare^#(#0(), #neg(@y)) -> c_57() , 51: #compare^#(#0(), #pos(@y)) -> c_58() , 52: #compare^#(#0(), #s(@y)) -> c_59() , 53: #compare^#(#neg(@x), #0()) -> c_60() , 54: #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , 55: #compare^#(#neg(@x), #pos(@y)) -> c_62() , 56: #compare^#(#pos(@x), #0()) -> c_63() , 57: #compare^#(#pos(@x), #neg(@y)) -> c_64() , 58: #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , 59: #compare^#(#s(@x), #0()) -> c_66() , 60: #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , 61: +^#(@x, @y) -> c_7(#add^#(@x, @y)) , 62: #add^#(#0(), @y) -> c_71() , 63: #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , 64: #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 65: #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , 66: #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 67: firstline#1^#(nil()) -> c_10() , 68: lcs#3^#(::(@len, @_@1)) -> c_16() , 69: lcstable#3^#(nil(), @l2, @x) -> c_22() , 70: newline#1^#(nil(), @lastline, @y) -> c_28() , 71: max#1^#(#false(), @a, @b) -> c_25() , 72: max#1^#(#true(), @a, @b) -> c_26() , 73: newline#2^#(nil(), @x, @xs, @y) -> c_30() , 74: right#1^#(::(@x, @xs)) -> c_38() , 75: newline#6^#(@elem, @nl) -> c_37() , 76: #and^#(#false(), #false()) -> c_84() , 77: #and^#(#false(), #true()) -> c_85() , 78: #and^#(#true(), #false()) -> c_86() , 79: #and^#(#true(), #true()) -> c_87() , 80: #pred^#(#0()) -> c_76() , 81: #pred^#(#neg(#s(@x))) -> c_77() , 82: #pred^#(#pos(#s(#0()))) -> c_78() , 83: #pred^#(#pos(#s(#s(@x)))) -> c_79() , 84: #succ^#(#0()) -> c_80() , 85: #succ^#(#neg(#s(#0()))) -> c_81() , 86: #succ^#(#neg(#s(#s(@x)))) -> c_82() , 87: #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) } Weak DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {8,16,18} by applications of Pre({8,16,18}) = {4,14,15,17}. Here rules are labeled as follows: DPs: { 1: firstline^#(@l) -> c_8(firstline#1^#(@l)) , 2: firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , 3: lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , 4: lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , 5: lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , 6: lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 7: lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , 8: lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , 9: lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , 10: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , 11: newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , 12: newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , 13: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , 14: newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , 15: newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , 16: right^#(@l) -> c_32(right#1^#(@l)) , 17: newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , 18: newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , 19: #abs^#(#0()) -> c_1() , 20: #abs^#(#neg(@x)) -> c_2() , 21: #abs^#(#pos(@x)) -> c_3() , 22: #abs^#(#s(@x)) -> c_4() , 23: #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , 24: #eq^#(#0(), #0()) -> c_40() , 25: #eq^#(#0(), #neg(@y)) -> c_41() , 26: #eq^#(#0(), #pos(@y)) -> c_42() , 27: #eq^#(#0(), #s(@y)) -> c_43() , 28: #eq^#(#neg(@x), #0()) -> c_44() , 29: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 30: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 31: #eq^#(#pos(@x), #0()) -> c_47() , 32: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 33: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 34: #eq^#(#s(@x), #0()) -> c_50() , 35: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 36: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 37: #eq^#(::(@x_1, @x_2), nil()) -> c_53() , 38: #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , 39: #eq^#(nil(), nil()) -> c_55() , 40: #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 41: #ckgt^#(#EQ()) -> c_68() , 42: #ckgt^#(#GT()) -> c_69() , 43: #ckgt^#(#LT()) -> c_70() , 44: #compare^#(#0(), #0()) -> c_56() , 45: #compare^#(#0(), #neg(@y)) -> c_57() , 46: #compare^#(#0(), #pos(@y)) -> c_58() , 47: #compare^#(#0(), #s(@y)) -> c_59() , 48: #compare^#(#neg(@x), #0()) -> c_60() , 49: #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , 50: #compare^#(#neg(@x), #pos(@y)) -> c_62() , 51: #compare^#(#pos(@x), #0()) -> c_63() , 52: #compare^#(#pos(@x), #neg(@y)) -> c_64() , 53: #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , 54: #compare^#(#s(@x), #0()) -> c_66() , 55: #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , 56: +^#(@x, @y) -> c_7(#add^#(@x, @y)) , 57: #add^#(#0(), @y) -> c_71() , 58: #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , 59: #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 60: #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , 61: #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 62: firstline#1^#(nil()) -> c_10() , 63: lcs#2^#(nil()) -> c_15(#abs^#(#0())) , 64: lcs#3^#(::(@len, @_@1)) -> c_16() , 65: lcs#3^#(nil()) -> c_17(#abs^#(#0())) , 66: lcstable#3^#(nil(), @l2, @x) -> c_22() , 67: newline#1^#(nil(), @lastline, @y) -> c_28() , 68: max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , 69: max#1^#(#false(), @a, @b) -> c_25() , 70: max#1^#(#true(), @a, @b) -> c_26() , 71: newline#2^#(nil(), @x, @xs, @y) -> c_30() , 72: right#1^#(::(@x, @xs)) -> c_38() , 73: right#1^#(nil()) -> c_39(#abs^#(#0())) , 74: newline#6^#(@elem, @nl) -> c_37() , 75: newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , 76: #and^#(#false(), #false()) -> c_84() , 77: #and^#(#false(), #true()) -> c_85() , 78: #and^#(#true(), #false()) -> c_86() , 79: #and^#(#true(), #true()) -> c_87() , 80: #pred^#(#0()) -> c_76() , 81: #pred^#(#neg(#s(@x))) -> c_77() , 82: #pred^#(#pos(#s(#0()))) -> c_78() , 83: #pred^#(#pos(#s(#s(@x)))) -> c_79() , 84: #succ^#(#0()) -> c_80() , 85: #succ^#(#neg(#s(#0()))) -> c_81() , 86: #succ^#(#neg(#s(#s(@x)))) -> c_82() , 87: #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) } Weak DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,15} by applications of Pre({4,15}) = {3,14}. Here rules are labeled as follows: DPs: { 1: firstline^#(@l) -> c_8(firstline#1^#(@l)) , 2: firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , 3: lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , 4: lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , 5: lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , 6: lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 7: lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , 8: lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , 9: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , 10: newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , 11: newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , 12: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , 13: newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , 14: newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , 15: newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , 16: #abs^#(#0()) -> c_1() , 17: #abs^#(#neg(@x)) -> c_2() , 18: #abs^#(#pos(@x)) -> c_3() , 19: #abs^#(#s(@x)) -> c_4() , 20: #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , 21: #eq^#(#0(), #0()) -> c_40() , 22: #eq^#(#0(), #neg(@y)) -> c_41() , 23: #eq^#(#0(), #pos(@y)) -> c_42() , 24: #eq^#(#0(), #s(@y)) -> c_43() , 25: #eq^#(#neg(@x), #0()) -> c_44() , 26: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 27: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 28: #eq^#(#pos(@x), #0()) -> c_47() , 29: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 30: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 31: #eq^#(#s(@x), #0()) -> c_50() , 32: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 33: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 34: #eq^#(::(@x_1, @x_2), nil()) -> c_53() , 35: #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , 36: #eq^#(nil(), nil()) -> c_55() , 37: #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 38: #ckgt^#(#EQ()) -> c_68() , 39: #ckgt^#(#GT()) -> c_69() , 40: #ckgt^#(#LT()) -> c_70() , 41: #compare^#(#0(), #0()) -> c_56() , 42: #compare^#(#0(), #neg(@y)) -> c_57() , 43: #compare^#(#0(), #pos(@y)) -> c_58() , 44: #compare^#(#0(), #s(@y)) -> c_59() , 45: #compare^#(#neg(@x), #0()) -> c_60() , 46: #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , 47: #compare^#(#neg(@x), #pos(@y)) -> c_62() , 48: #compare^#(#pos(@x), #0()) -> c_63() , 49: #compare^#(#pos(@x), #neg(@y)) -> c_64() , 50: #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , 51: #compare^#(#s(@x), #0()) -> c_66() , 52: #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , 53: +^#(@x, @y) -> c_7(#add^#(@x, @y)) , 54: #add^#(#0(), @y) -> c_71() , 55: #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , 56: #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 57: #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , 58: #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 59: firstline#1^#(nil()) -> c_10() , 60: lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , 61: lcs#2^#(nil()) -> c_15(#abs^#(#0())) , 62: lcs#3^#(::(@len, @_@1)) -> c_16() , 63: lcs#3^#(nil()) -> c_17(#abs^#(#0())) , 64: lcstable#3^#(nil(), @l2, @x) -> c_22() , 65: newline#1^#(nil(), @lastline, @y) -> c_28() , 66: max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , 67: max#1^#(#false(), @a, @b) -> c_25() , 68: max#1^#(#true(), @a, @b) -> c_26() , 69: newline#2^#(nil(), @x, @xs, @y) -> c_30() , 70: right^#(@l) -> c_32(right#1^#(@l)) , 71: right#1^#(::(@x, @xs)) -> c_38() , 72: right#1^#(nil()) -> c_39(#abs^#(#0())) , 73: newline#6^#(@elem, @nl) -> c_37() , 74: newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , 75: newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , 76: #and^#(#false(), #false()) -> c_84() , 77: #and^#(#false(), #true()) -> c_85() , 78: #and^#(#true(), #false()) -> c_86() , 79: #and^#(#true(), #true()) -> c_87() , 80: #pred^#(#0()) -> c_76() , 81: #pred^#(#neg(#s(@x))) -> c_77() , 82: #pred^#(#pos(#s(#0()))) -> c_78() , 83: #pred^#(#pos(#s(#s(@x)))) -> c_79() , 84: #succ^#(#0()) -> c_80() , 85: #succ^#(#neg(#s(#0()))) -> c_81() , 86: #succ^#(#neg(#s(#s(@x)))) -> c_82() , 87: #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) } Weak DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {13} by applications of Pre({13}) = {12}. Here rules are labeled as follows: DPs: { 1: firstline^#(@l) -> c_8(firstline#1^#(@l)) , 2: firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , 3: lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , 4: lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , 5: lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 6: lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , 7: lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , 8: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , 9: newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , 10: newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , 11: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , 12: newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , 13: newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , 14: #abs^#(#0()) -> c_1() , 15: #abs^#(#neg(@x)) -> c_2() , 16: #abs^#(#pos(@x)) -> c_3() , 17: #abs^#(#s(@x)) -> c_4() , 18: #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , 19: #eq^#(#0(), #0()) -> c_40() , 20: #eq^#(#0(), #neg(@y)) -> c_41() , 21: #eq^#(#0(), #pos(@y)) -> c_42() , 22: #eq^#(#0(), #s(@y)) -> c_43() , 23: #eq^#(#neg(@x), #0()) -> c_44() , 24: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 25: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 26: #eq^#(#pos(@x), #0()) -> c_47() , 27: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 28: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 29: #eq^#(#s(@x), #0()) -> c_50() , 30: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 31: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 32: #eq^#(::(@x_1, @x_2), nil()) -> c_53() , 33: #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , 34: #eq^#(nil(), nil()) -> c_55() , 35: #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 36: #ckgt^#(#EQ()) -> c_68() , 37: #ckgt^#(#GT()) -> c_69() , 38: #ckgt^#(#LT()) -> c_70() , 39: #compare^#(#0(), #0()) -> c_56() , 40: #compare^#(#0(), #neg(@y)) -> c_57() , 41: #compare^#(#0(), #pos(@y)) -> c_58() , 42: #compare^#(#0(), #s(@y)) -> c_59() , 43: #compare^#(#neg(@x), #0()) -> c_60() , 44: #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , 45: #compare^#(#neg(@x), #pos(@y)) -> c_62() , 46: #compare^#(#pos(@x), #0()) -> c_63() , 47: #compare^#(#pos(@x), #neg(@y)) -> c_64() , 48: #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , 49: #compare^#(#s(@x), #0()) -> c_66() , 50: #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , 51: +^#(@x, @y) -> c_7(#add^#(@x, @y)) , 52: #add^#(#0(), @y) -> c_71() , 53: #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , 54: #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 55: #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , 56: #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 57: firstline#1^#(nil()) -> c_10() , 58: lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , 59: lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , 60: lcs#2^#(nil()) -> c_15(#abs^#(#0())) , 61: lcs#3^#(::(@len, @_@1)) -> c_16() , 62: lcs#3^#(nil()) -> c_17(#abs^#(#0())) , 63: lcstable#3^#(nil(), @l2, @x) -> c_22() , 64: newline#1^#(nil(), @lastline, @y) -> c_28() , 65: max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , 66: max#1^#(#false(), @a, @b) -> c_25() , 67: max#1^#(#true(), @a, @b) -> c_26() , 68: newline#2^#(nil(), @x, @xs, @y) -> c_30() , 69: right^#(@l) -> c_32(right#1^#(@l)) , 70: right#1^#(::(@x, @xs)) -> c_38() , 71: right#1^#(nil()) -> c_39(#abs^#(#0())) , 72: newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , 73: newline#6^#(@elem, @nl) -> c_37() , 74: newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , 75: newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , 76: #and^#(#false(), #false()) -> c_84() , 77: #and^#(#false(), #true()) -> c_85() , 78: #and^#(#true(), #false()) -> c_86() , 79: #and^#(#true(), #true()) -> c_87() , 80: #pred^#(#0()) -> c_76() , 81: #pred^#(#neg(#s(@x))) -> c_77() , 82: #pred^#(#pos(#s(#0()))) -> c_78() , 83: #pred^#(#pos(#s(#s(@x)))) -> c_79() , 84: #succ^#(#0()) -> c_80() , 85: #succ^#(#neg(#s(#0()))) -> c_81() , 86: #succ^#(#neg(#s(#s(@x)))) -> c_82() , 87: #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) } Weak DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {12} by applications of Pre({12}) = {11}. Here rules are labeled as follows: DPs: { 1: firstline^#(@l) -> c_8(firstline#1^#(@l)) , 2: firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , 3: lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , 4: lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , 5: lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 6: lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , 7: lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , 8: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , 9: newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , 10: newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , 11: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) , 12: newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , 13: #abs^#(#0()) -> c_1() , 14: #abs^#(#neg(@x)) -> c_2() , 15: #abs^#(#pos(@x)) -> c_3() , 16: #abs^#(#s(@x)) -> c_4() , 17: #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , 18: #eq^#(#0(), #0()) -> c_40() , 19: #eq^#(#0(), #neg(@y)) -> c_41() , 20: #eq^#(#0(), #pos(@y)) -> c_42() , 21: #eq^#(#0(), #s(@y)) -> c_43() , 22: #eq^#(#neg(@x), #0()) -> c_44() , 23: #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , 24: #eq^#(#neg(@x), #pos(@y)) -> c_46() , 25: #eq^#(#pos(@x), #0()) -> c_47() , 26: #eq^#(#pos(@x), #neg(@y)) -> c_48() , 27: #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , 28: #eq^#(#s(@x), #0()) -> c_50() , 29: #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , 30: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 31: #eq^#(::(@x_1, @x_2), nil()) -> c_53() , 32: #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , 33: #eq^#(nil(), nil()) -> c_55() , 34: #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 35: #ckgt^#(#EQ()) -> c_68() , 36: #ckgt^#(#GT()) -> c_69() , 37: #ckgt^#(#LT()) -> c_70() , 38: #compare^#(#0(), #0()) -> c_56() , 39: #compare^#(#0(), #neg(@y)) -> c_57() , 40: #compare^#(#0(), #pos(@y)) -> c_58() , 41: #compare^#(#0(), #s(@y)) -> c_59() , 42: #compare^#(#neg(@x), #0()) -> c_60() , 43: #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , 44: #compare^#(#neg(@x), #pos(@y)) -> c_62() , 45: #compare^#(#pos(@x), #0()) -> c_63() , 46: #compare^#(#pos(@x), #neg(@y)) -> c_64() , 47: #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , 48: #compare^#(#s(@x), #0()) -> c_66() , 49: #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , 50: +^#(@x, @y) -> c_7(#add^#(@x, @y)) , 51: #add^#(#0(), @y) -> c_71() , 52: #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , 53: #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 54: #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , 55: #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 56: firstline#1^#(nil()) -> c_10() , 57: lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , 58: lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , 59: lcs#2^#(nil()) -> c_15(#abs^#(#0())) , 60: lcs#3^#(::(@len, @_@1)) -> c_16() , 61: lcs#3^#(nil()) -> c_17(#abs^#(#0())) , 62: lcstable#3^#(nil(), @l2, @x) -> c_22() , 63: newline#1^#(nil(), @lastline, @y) -> c_28() , 64: max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , 65: max#1^#(#false(), @a, @b) -> c_25() , 66: max#1^#(#true(), @a, @b) -> c_26() , 67: newline#2^#(nil(), @x, @xs, @y) -> c_30() , 68: newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , 69: right^#(@l) -> c_32(right#1^#(@l)) , 70: right#1^#(::(@x, @xs)) -> c_38() , 71: right#1^#(nil()) -> c_39(#abs^#(#0())) , 72: newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , 73: newline#6^#(@elem, @nl) -> c_37() , 74: newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , 75: newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , 76: #and^#(#false(), #false()) -> c_84() , 77: #and^#(#false(), #true()) -> c_85() , 78: #and^#(#true(), #false()) -> c_86() , 79: #and^#(#true(), #true()) -> c_87() , 80: #pred^#(#0()) -> c_76() , 81: #pred^#(#neg(#s(@x))) -> c_77() , 82: #pred^#(#pos(#s(#0()))) -> c_78() , 83: #pred^#(#pos(#s(#s(@x)))) -> c_79() , 84: #succ^#(#0()) -> c_80() , 85: #succ^#(#neg(#s(#0()))) -> c_81() , 86: #succ^#(#neg(#s(#s(@x)))) -> c_82() , 87: #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) } Weak DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #equal^#(@x, @y) -> c_5(#eq^#(@x, @y)) , #eq^#(#0(), #0()) -> c_40() , #eq^#(#0(), #neg(@y)) -> c_41() , #eq^#(#0(), #pos(@y)) -> c_42() , #eq^#(#0(), #s(@y)) -> c_43() , #eq^#(#neg(@x), #0()) -> c_44() , #eq^#(#neg(@x), #neg(@y)) -> c_45(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_46() , #eq^#(#pos(@x), #0()) -> c_47() , #eq^#(#pos(@x), #neg(@y)) -> c_48() , #eq^#(#pos(@x), #pos(@y)) -> c_49(#eq^#(@x, @y)) , #eq^#(#s(@x), #0()) -> c_50() , #eq^#(#s(@x), #s(@y)) -> c_51(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_52(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_53() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_54() , #eq^#(nil(), nil()) -> c_55() , #greater^#(@x, @y) -> c_6(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_68() , #ckgt^#(#GT()) -> c_69() , #ckgt^#(#LT()) -> c_70() , #compare^#(#0(), #0()) -> c_56() , #compare^#(#0(), #neg(@y)) -> c_57() , #compare^#(#0(), #pos(@y)) -> c_58() , #compare^#(#0(), #s(@y)) -> c_59() , #compare^#(#neg(@x), #0()) -> c_60() , #compare^#(#neg(@x), #neg(@y)) -> c_61(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_62() , #compare^#(#pos(@x), #0()) -> c_63() , #compare^#(#pos(@x), #neg(@y)) -> c_64() , #compare^#(#pos(@x), #pos(@y)) -> c_65(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_66() , #compare^#(#s(@x), #s(@y)) -> c_67(#compare^#(@x, @y)) , +^#(@x, @y) -> c_7(#add^#(@x, @y)) , #add^#(#0(), @y) -> c_71() , #add^#(#neg(#s(#0())), @y) -> c_72(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_73(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_74(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_75(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , firstline#1^#(nil()) -> c_10() , lcs#1^#(@m) -> c_13(lcs#2^#(@m)) , lcs#2^#(::(@l1, @_@2)) -> c_14(lcs#3^#(@l1)) , lcs#2^#(nil()) -> c_15(#abs^#(#0())) , lcs#3^#(::(@len, @_@1)) -> c_16() , lcs#3^#(nil()) -> c_17(#abs^#(#0())) , lcstable#3^#(nil(), @l2, @x) -> c_22() , newline#1^#(nil(), @lastline, @y) -> c_28() , max^#(@a, @b) -> c_24(max#1^#(#greater(@a, @b), @a, @b), #greater^#(@a, @b)) , max#1^#(#false(), @a, @b) -> c_25() , max#1^#(#true(), @a, @b) -> c_26() , newline#2^#(nil(), @x, @xs, @y) -> c_30() , newline#3^#(@nl, @belowVal, @lastline', @x, @y) -> c_31(newline#4^#(right(@nl), @belowVal, @lastline', @nl, @x, @y), right^#(@nl)) , newline#4^#(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> c_33(newline#5^#(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y), right^#(@lastline')) , right^#(@l) -> c_32(right#1^#(@l)) , right#1^#(::(@x, @xs)) -> c_38() , right#1^#(nil()) -> c_39(#abs^#(#0())) , newline#5^#(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> c_34(newline#6^#(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl), newline#7^#(#equal(@x, @y), @belowVal, @diagVal, @rightVal), #equal^#(@x, @y)) , newline#6^#(@elem, @nl) -> c_37() , newline#7^#(#false(), @belowVal, @diagVal, @rightVal) -> c_35(max^#(@belowVal, @rightVal)) , newline#7^#(#true(), @belowVal, @diagVal, @rightVal) -> c_36(+^#(@diagVal, #pos(#s(#0())))) , #and^#(#false(), #false()) -> c_84() , #and^#(#false(), #true()) -> c_85() , #and^#(#true(), #false()) -> c_86() , #and^#(#true(), #true()) -> c_87() , #pred^#(#0()) -> c_76() , #pred^#(#neg(#s(@x))) -> c_77() , #pred^#(#pos(#s(#0()))) -> c_78() , #pred^#(#pos(#s(#s(@x)))) -> c_79() , #succ^#(#0()) -> c_80() , #succ^#(#neg(#s(#0()))) -> c_81() , #succ^#(#neg(#s(#s(@x)))) -> c_82() , #succ^#(#pos(#s(@x))) -> c_83() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_8(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , lcstable^#(@l1, @l2) -> c_12(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_18(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_19(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_20(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_21(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_23(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_27(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { firstline#1^#(::(@x, @xs)) -> c_9(#abs^#(#0()), firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_11(lcs#1^#(lcstable(@l1, @l2)), lcstable^#(@l1, @l2)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_29(newline#3^#(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y), newline^#(@y, @lastline', @xs)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_1(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) , lcs^#(@l1, @l2) -> c_3(lcstable^#(@l1, @l2)) , lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: firstline^#(@l) -> c_1(firstline#1^#(@l)) -->_1 firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) :2 2: firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) -->_1 firstline^#(@l) -> c_1(firstline#1^#(@l)) :1 3: lcs^#(@l1, @l2) -> c_3(lcstable^#(@l1, @l2)) -->_1 lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) :4 4: lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) -->_1 lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) :6 -->_1 lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) :5 5: lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) -->_1 lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) :7 -->_2 lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) :4 6: lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) -->_1 firstline^#(@l) -> c_1(firstline#1^#(@l)) :1 7: lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) -->_1 lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) :8 8: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) -->_1 newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) :9 9: newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) -->_1 newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) :10 10: newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) -->_1 newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) :11 11: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) -->_1 newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) :9 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { lcs^#(@l1, @l2) -> c_3(lcstable^#(@l1, @l2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_1(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) , lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcs(@l1, @l2) -> lcs#1(lcstable(@l1, @l2)) , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcs#1(@m) -> lcs#2(@m) , lcs#2(::(@l1, @_@2)) -> lcs#3(@l1) , lcs#2(nil()) -> #abs(#0()) , lcs#3(::(@len, @_@1)) -> @len , lcs#3(nil()) -> #abs(#0()) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_1(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) , lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) } Trs: { firstline(@l) -> firstline#1(@l) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#abs](x1) = [0] [#neg](x1) = [0] [#pos](x1) = [0] [#s](x1) = [0] [#equal](x1, x2) = [0] [#eq](x1, x2) = [0] [#greater](x1, x2) = [0] [#compare](x1, x2) = [0] [#ckgt](x1) = [0] [+](x1, x2) = [2] x1 + [0] [#add](x1, x2) = [0] [firstline](x1) = [2] [firstline#1](x1) = [0] [::](x1, x2) = [1] x1 + [1] x2 + [2] [nil] = [0] [lcs](x1, x2) = [0] [lcstable](x1, x2) = [0] [lcs#1](x1) = [0] [lcs#2](x1) = [0] [lcs#3](x1) = [0] [lcstable#1](x1, x2) = [1] x2 + [0] [lcstable#2](x1, x2, x3) = [0] [lcstable#3](x1, x2, x3) = [0] [newline](x1, x2, x3) = [0] [max](x1, x2) = [0] [max#1](x1, x2, x3) = [0] [#false] = [0] [#true] = [0] [newline#1](x1, x2, x3) = [2] x2 + [2] x3 + [0] [newline#2](x1, x2, x3, x4) = [0] [newline#3](x1, x2, x3, x4, x5) = [2] x2 + [2] x4 + [0] [right](x1) = [0] [newline#4](x1, x2, x3, x4, x5, x6) = [2] x2 + [2] x5 + [2] x6 + [0] [newline#5](x1, x2, x3, x4, x5, x6) = [0] [newline#7](x1, x2, x3, x4) = [0] [newline#6](x1, x2) = [0] [right#1](x1) = [0] [#pred](x1) = [0] [#succ](x1) = [0] [#and](x1, x2) = [0] [#EQ] = [0] [#GT] = [0] [#LT] = [0] [#abs^#](x1) = [0] [c_1] = [0] [c_2] = [0] [c_3] = [0] [c_4] = [0] [#equal^#](x1, x2) = [0] [c_5](x1) = [0] [#eq^#](x1, x2) = [0] [#greater^#](x1, x2) = [0] [c_6](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [+^#](x1, x2) = [0] [c_7](x1) = [0] [#add^#](x1, x2) = [0] [firstline^#](x1) = [2] x1 + [0] [c_8](x1) = [0] [firstline#1^#](x1) = [2] x1 + [0] [c_9](x1, x2) = [0] [c_10] = [0] [lcs^#](x1, x2) = [0] [c_11](x1, x2) = [0] [lcs#1^#](x1) = [0] [lcstable^#](x1, x2) = [2] x2 + [0] [c_12](x1) = [0] [lcstable#1^#](x1, x2) = [2] x2 + [0] [c_13](x1) = [0] [lcs#2^#](x1) = [0] [c_14](x1) = [0] [lcs#3^#](x1) = [0] [c_15](x1) = [0] [c_16] = [0] [c_17](x1) = [0] [c_18](x1, x2) = [0] [lcstable#2^#](x1, x2, x3) = [0] [c_19](x1) = [0] [c_20](x1) = [0] [lcstable#3^#](x1, x2, x3) = [0] [c_21](x1) = [0] [newline^#](x1, x2, x3) = [0] [c_22] = [0] [c_23](x1) = [0] [newline#1^#](x1, x2, x3) = [0] [max^#](x1, x2) = [0] [c_24](x1, x2) = [0] [max#1^#](x1, x2, x3) = [0] [c_25] = [0] [c_26] = [0] [c_27](x1) = [0] [newline#2^#](x1, x2, x3, x4) = [0] [c_28] = [0] [c_29](x1, x2) = [0] [newline#3^#](x1, x2, x3, x4, x5) = [0] [c_30] = [0] [c_31](x1, x2) = [0] [newline#4^#](x1, x2, x3, x4, x5, x6) = [0] [right^#](x1) = [0] [c_32](x1) = [0] [right#1^#](x1) = [0] [c_33](x1, x2) = [0] [newline#5^#](x1, x2, x3, x4, x5, x6) = [0] [c_34](x1, x2, x3) = [0] [newline#6^#](x1, x2) = [0] [newline#7^#](x1, x2, x3, x4) = [0] [c_35](x1) = [0] [c_36](x1) = [0] [c_37] = [0] [c_38] = [0] [c_39](x1) = [0] [c_40] = [0] [c_41] = [0] [c_42] = [0] [c_43] = [0] [c_44] = [0] [c_45](x1) = [0] [c_46] = [0] [c_47] = [0] [c_48] = [0] [c_49](x1) = [0] [c_50] = [0] [c_51](x1) = [0] [c_52](x1, x2, x3) = [0] [#and^#](x1, x2) = [0] [c_53] = [0] [c_54] = [0] [c_55] = [0] [c_56] = [0] [c_57] = [0] [c_58] = [0] [c_59] = [0] [c_60] = [0] [c_61](x1) = [0] [c_62] = [0] [c_63] = [0] [c_64] = [0] [c_65](x1) = [0] [c_66] = [0] [c_67](x1) = [0] [c_68] = [0] [c_69] = [0] [c_70] = [0] [c_71] = [0] [c_72](x1) = [0] [#pred^#](x1) = [0] [c_73](x1, x2) = [0] [c_74](x1) = [0] [#succ^#](x1) = [0] [c_75](x1, x2) = [0] [c_76] = [0] [c_77] = [0] [c_78] = [0] [c_79] = [0] [c_80] = [0] [c_81] = [0] [c_82] = [0] [c_83] = [0] [c_84] = [0] [c_85] = [0] [c_86] = [0] [c_87] = [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [2] [c_3](x1) = [0] [c_4](x1) = [1] x1 + [0] [c_5](x1, x2) = [2] x1 + [1] x2 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1) = [1] x1 + [0] [c_8](x1) = [2] x1 + [0] [c_9](x1) = [1] x1 + [0] [c_10](x1) = [2] x1 + [0] [c_11](x1) = [2] x1 + [0] This order satisfies following ordering constraints [firstline^#(@l)] = [2] @l + [0] >= [2] @l + [0] = [c_1(firstline#1^#(@l))] [firstline#1^#(::(@x, @xs))] = [2] @x + [2] @xs + [4] > [2] @xs + [2] = [c_2(firstline^#(@xs))] [lcstable^#(@l1, @l2)] = [2] @l2 + [0] >= [2] @l2 + [0] = [c_4(lcstable#1^#(@l1, @l2))] [lcstable#1^#(::(@x, @xs), @l2)] = [2] @l2 + [0] >= [2] @l2 + [0] = [c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2))] [lcstable#1^#(nil(), @l2)] = [2] @l2 + [0] >= [2] @l2 + [0] = [c_6(firstline^#(@l2))] [lcstable#2^#(@m, @l2, @x)] = [0] >= [0] = [c_7(lcstable#3^#(@m, @l2, @x))] [lcstable#3^#(::(@l, @ls), @l2, @x)] = [0] >= [0] = [c_8(newline^#(@x, @l, @l2))] [newline^#(@y, @lastline, @l)] = [0] >= [0] = [c_9(newline#1^#(@l, @lastline, @y))] [newline#1^#(::(@x, @xs), @lastline, @y)] = [0] >= [0] = [c_10(newline#2^#(@lastline, @x, @xs, @y))] [newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y)] = [0] >= [0] = [c_11(newline^#(@y, @lastline', @xs))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { firstline^#(@l) -> c_1(firstline#1^#(@l)) , lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) , newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) } Weak DPs: { firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 3: lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 10: firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_4) = {1}, Uargs(c_5) = {1, 2}, Uargs(c_6) = {1}, Uargs(c_7) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1}, Uargs(c_10) = {1}, Uargs(c_11) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#abs](x1) = [0] [#neg](x1) = [0] [#pos](x1) = [0] [#s](x1) = [0] [#equal](x1, x2) = [0] [#eq](x1, x2) = [0] [#greater](x1, x2) = [1] x1 + [1] x2 + [0] [#compare](x1, x2) = [0] [#ckgt](x1) = [0] [+](x1, x2) = [2] x1 + [0] [#add](x1, x2) = [0] [firstline](x1) = [0] [firstline#1](x1) = [0] [::](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [0] [lcs](x1, x2) = [0] [lcstable](x1, x2) = [0] [lcs#1](x1) = [0] [lcs#2](x1) = [0] [lcs#3](x1) = [0] [lcstable#1](x1, x2) = [1] x2 + [0] [lcstable#2](x1, x2, x3) = [0] [lcstable#3](x1, x2, x3) = [0] [newline](x1, x2, x3) = [2] [max](x1, x2) = [0] [max#1](x1, x2, x3) = [0] [#false] = [0] [#true] = [0] [newline#1](x1, x2, x3) = [2] x2 + [2] x3 + [0] [newline#2](x1, x2, x3, x4) = [0] [newline#3](x1, x2, x3, x4, x5) = [2] x4 + [0] [right](x1) = [0] [newline#4](x1, x2, x3, x4, x5, x6) = [2] x2 + [2] x5 + [2] x6 + [0] [newline#5](x1, x2, x3, x4, x5, x6) = [2] x3 + [0] [newline#7](x1, x2, x3, x4) = [0] [newline#6](x1, x2) = [0] [right#1](x1) = [0] [#pred](x1) = [0] [#succ](x1) = [0] [#and](x1, x2) = [0] [#EQ] = [0] [#GT] = [0] [#LT] = [0] [#abs^#](x1) = [0] [c_1] = [0] [c_2] = [0] [c_3] = [0] [c_4] = [0] [#equal^#](x1, x2) = [0] [c_5](x1) = [0] [#eq^#](x1, x2) = [0] [#greater^#](x1, x2) = [0] [c_6](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [+^#](x1, x2) = [0] [c_7](x1) = [0] [#add^#](x1, x2) = [0] [firstline^#](x1) = [1] x1 + [0] [c_8](x1) = [0] [firstline#1^#](x1) = [1] x1 + [0] [c_9](x1, x2) = [0] [c_10] = [0] [lcs^#](x1, x2) = [0] [c_11](x1, x2) = [0] [lcs#1^#](x1) = [0] [lcstable^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_12](x1) = [0] [lcstable#1^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_13](x1) = [0] [lcs#2^#](x1) = [0] [c_14](x1) = [0] [lcs#3^#](x1) = [0] [c_15](x1) = [0] [c_16] = [0] [c_17](x1) = [0] [c_18](x1, x2) = [0] [lcstable#2^#](x1, x2, x3) = [0] [c_19](x1) = [0] [c_20](x1) = [0] [lcstable#3^#](x1, x2, x3) = [0] [c_21](x1) = [0] [newline^#](x1, x2, x3) = [0] [c_22] = [0] [c_23](x1) = [0] [newline#1^#](x1, x2, x3) = [0] [max^#](x1, x2) = [0] [c_24](x1, x2) = [0] [max#1^#](x1, x2, x3) = [0] [c_25] = [0] [c_26] = [0] [c_27](x1) = [0] [newline#2^#](x1, x2, x3, x4) = [0] [c_28] = [0] [c_29](x1, x2) = [0] [newline#3^#](x1, x2, x3, x4, x5) = [0] [c_30] = [0] [c_31](x1, x2) = [0] [newline#4^#](x1, x2, x3, x4, x5, x6) = [0] [right^#](x1) = [0] [c_32](x1) = [0] [right#1^#](x1) = [0] [c_33](x1, x2) = [0] [newline#5^#](x1, x2, x3, x4, x5, x6) = [0] [c_34](x1, x2, x3) = [0] [newline#6^#](x1, x2) = [0] [newline#7^#](x1, x2, x3, x4) = [0] [c_35](x1) = [0] [c_36](x1) = [0] [c_37] = [0] [c_38] = [0] [c_39](x1) = [0] [c_40] = [0] [c_41] = [0] [c_42] = [0] [c_43] = [0] [c_44] = [0] [c_45](x1) = [0] [c_46] = [0] [c_47] = [0] [c_48] = [0] [c_49](x1) = [0] [c_50] = [0] [c_51](x1) = [0] [c_52](x1, x2, x3) = [0] [#and^#](x1, x2) = [0] [c_53] = [0] [c_54] = [0] [c_55] = [0] [c_56] = [0] [c_57] = [0] [c_58] = [0] [c_59] = [0] [c_60] = [0] [c_61](x1) = [0] [c_62] = [0] [c_63] = [0] [c_64] = [0] [c_65](x1) = [0] [c_66] = [0] [c_67](x1) = [0] [c_68] = [0] [c_69] = [0] [c_70] = [0] [c_71] = [0] [c_72](x1) = [0] [#pred^#](x1) = [0] [c_73](x1, x2) = [0] [c_74](x1) = [0] [#succ^#](x1) = [0] [c_75](x1, x2) = [0] [c_76] = [0] [c_77] = [0] [c_78] = [0] [c_79] = [0] [c_80] = [0] [c_81] = [0] [c_82] = [0] [c_83] = [0] [c_84] = [0] [c_85] = [0] [c_86] = [0] [c_87] = [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1) = [0] [c_4](x1) = [1] x1 + [0] [c_5](x1, x2) = [2] x1 + [1] x2 + [0] [c_6](x1) = [1] x1 + [0] [c_7](x1) = [1] x1 + [0] [c_8](x1) = [2] x1 + [0] [c_9](x1) = [1] x1 + [0] [c_10](x1) = [2] x1 + [0] [c_11](x1) = [2] x1 + [0] This order satisfies following ordering constraints [firstline^#(@l)] = [1] @l + [0] >= [1] @l + [0] = [c_1(firstline#1^#(@l))] [firstline#1^#(::(@x, @xs))] = [1] @x + [1] @xs + [1] > [1] @xs + [0] = [c_2(firstline^#(@xs))] [lcstable^#(@l1, @l2)] = [1] @l1 + [1] @l2 + [0] >= [1] @l1 + [1] @l2 + [0] = [c_4(lcstable#1^#(@l1, @l2))] [lcstable#1^#(::(@x, @xs), @l2)] = [1] @l2 + [1] @x + [1] @xs + [1] > [1] @l2 + [1] @xs + [0] = [c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2))] [lcstable#1^#(nil(), @l2)] = [1] @l2 + [0] >= [1] @l2 + [0] = [c_6(firstline^#(@l2))] [lcstable#2^#(@m, @l2, @x)] = [0] >= [0] = [c_7(lcstable#3^#(@m, @l2, @x))] [lcstable#3^#(::(@l, @ls), @l2, @x)] = [0] >= [0] = [c_8(newline^#(@x, @l, @l2))] [newline^#(@y, @lastline, @l)] = [0] >= [0] = [c_9(newline#1^#(@l, @lastline, @y))] [newline#1^#(::(@x, @xs), @lastline, @y)] = [0] >= [0] = [c_10(newline#2^#(@lastline, @x, @xs, @y))] [newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y)] = [0] >= [0] = [c_11(newline^#(@y, @lastline', @xs))] Consider the set of all dependency pairs DPs: { 1: firstline^#(@l) -> c_1(firstline#1^#(@l)) , 2: lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , 3: lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , 4: lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) , 5: lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , 6: lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) , 7: newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , 8: newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , 9: newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) , 10: firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {3,10}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,10}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Strict DPs: { newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) } Weak DPs: { firstline^#(@l) -> c_1(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) , lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) , lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { firstline^#(@l) -> c_1(firstline#1^#(@l)) , firstline#1^#(::(@x, @xs)) -> c_2(firstline^#(@xs)) , lcstable#1^#(nil(), @l2) -> c_6(firstline^#(@l2)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { newline^#(@y, @lastline, @l) -> c_9(newline#1^#(@l, @lastline, @y)) , newline#1^#(::(@x, @xs), @lastline, @y) -> c_10(newline#2^#(@lastline, @x, @xs, @y)) , newline#2^#(::(@belowVal, @lastline'), @x, @xs, @y) -> c_11(newline^#(@y, @lastline', @xs)) } Weak DPs: { lcstable^#(@l1, @l2) -> c_4(lcstable#1^#(@l1, @l2)) , lcstable#1^#(::(@x, @xs), @l2) -> c_5(lcstable#2^#(lcstable(@xs, @l2), @l2, @x), lcstable^#(@xs, @l2)) , lcstable#2^#(@m, @l2, @x) -> c_7(lcstable#3^#(@m, @l2, @x)) , lcstable#3^#(::(@l, @ls), @l2, @x) -> c_8(newline^#(@x, @l, @l2)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #equal(@x, @y) -> #eq(@x, @y) , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#0(), #s(@y)) -> #false() , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , +(@x, @y) -> #add(@x, @y) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , firstline(@l) -> firstline#1(@l) , firstline#1(::(@x, @xs)) -> ::(#abs(#0()), firstline(@xs)) , firstline#1(nil()) -> nil() , lcstable(@l1, @l2) -> lcstable#1(@l1, @l2) , lcstable#1(::(@x, @xs), @l2) -> lcstable#2(lcstable(@xs, @l2), @l2, @x) , lcstable#1(nil(), @l2) -> ::(firstline(@l2), nil()) , lcstable#2(@m, @l2, @x) -> lcstable#3(@m, @l2, @x) , lcstable#3(::(@l, @ls), @l2, @x) -> ::(newline(@x, @l, @l2), ::(@l, @ls)) , lcstable#3(nil(), @l2, @x) -> nil() , newline(@y, @lastline, @l) -> newline#1(@l, @lastline, @y) , max(@a, @b) -> max#1(#greater(@a, @b), @a, @b) , max#1(#false(), @a, @b) -> @b , max#1(#true(), @a, @b) -> @a , newline#1(::(@x, @xs), @lastline, @y) -> newline#2(@lastline, @x, @xs, @y) , newline#1(nil(), @lastline, @y) -> nil() , newline#2(::(@belowVal, @lastline'), @x, @xs, @y) -> newline#3(newline(@y, @lastline', @xs), @belowVal, @lastline', @x, @y) , newline#2(nil(), @x, @xs, @y) -> nil() , newline#3(@nl, @belowVal, @lastline', @x, @y) -> newline#4(right(@nl), @belowVal, @lastline', @nl, @x, @y) , right(@l) -> right#1(@l) , newline#4(@rightVal, @belowVal, @lastline', @nl, @x, @y) -> newline#5(right(@lastline'), @belowVal, @nl, @rightVal, @x, @y) , newline#5(@diagVal, @belowVal, @nl, @rightVal, @x, @y) -> newline#6(newline#7(#equal(@x, @y), @belowVal, @diagVal, @rightVal), @nl) , newline#7(#false(), @belowVal, @diagVal, @rightVal) -> max(@belowVal, @rightVal) , newline#7(#true(), @belowVal, @diagVal, @rightVal) -> +(@diagVal, #pos(#s(#0()))) , newline#6(@elem, @nl) -> ::(@elem, @nl) , right#1(::(@x, @xs)) -> @x , right#1(nil()) -> #abs(#0()) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..